Higher-order logic, also known as simple type theory [3], has been described as the combination of functional programming and logic [9], and has proved a very powerful tool for the formalization of mathematics and computer science. It is an expressive enough logic to cover a wide array of fields, while still being built on relatively simple principles, and a number of proof assistants based on higher-order logic are available. We consider formal reasoning in the generic proof assistant Isabelle [10, 11]. In the present paper we are taking advantage of the genericity of Isabelle, but we also find that Isabelle is at least as user-friendly and intuitive as other proof assistants of comparable power. Although Isabelle is generic and comes with a number of object logics like first-order logic (FOL) and axiomatic set theory (ZF), the default object logic is higher-order logic, called Isabelle/HOL.

AI activities are also being pursued at other Schlumberger locations, often jointly with SDR The locations related to logging and interpretation include: Schlumberger-Doll Research, Ridgefield, Connecticut (Contact: Peter Wu'l); Schlumberger Well Services, Austin, Texas (Contact: Scott Gut/my); Schlumberger Well Services, Houston, Texas (Contact: Scott Ma&s); Nippon Schlumberger, K K, Tokyo, Japan (Contact: Dennzs O'NezU); I&ude et Production Schlumbcraer. Other Schlumberger companies involied in Ai research include! Expert Systems Current work in expert, systems is concerned with developing techniques for building more robust and versatile log interpretation systems. One shortcoming of "first generation" expert systems, such as the Dipmeter Advisor, is their inability to reason about the task that they attempt to perform. Any description of the overall task is usually procedurally encoded and unavailable for examination.

In addition to their limpid interface with semantics, categorial grammars enjoy another important property: learnability. This was first noticed by Buskowsky and Penn and further studied by Kanazawa, for Bar-Hillel categorial grammars. What about Lambek categorial grammars? In a previous paper we showed that product free Lambek grammars where learnable from structured sentences, the structures being incomplete natural deductions. These grammars were shown to be unlearnable from strings by Foret and Le Nir. In the present paper we show that Lambek grammars, possibly with product, are learnable from proof frames that are incomplete proof nets. After a short reminder on grammatical inference \`a la Gold, we provide an algorithm that learns Lambek grammars with product from proof frames and we prove its convergence. We do so for 1-valued also known as rigid Lambek grammars with product, since standard techniques can extend our result to $k$-valued grammars. Because of the correspondence between cut-free proof nets and normal natural deductions, our initial result on product free Lambek grammars can be recovered. We are sad to dedicate the present paper to Philippe Darondeau, with whom we started to study such questions in Rennes at the beginning of the millennium, and who passed away prematurely. We are glad to dedicate the present paper to Jim Lambek for his 90 birthday: he is the living proof that research is an eternal learning process.

Natural deduction, which is a method for establishing validity of propositional type arguments, helps develop important reasoning skills and is thus a key ingredient in a course on introductory logic. We present two core components, namely solution generation and practice problem generation, for enabling computer-aided education for this important subject domain. The key enabling technology is use of an offline-computed data-structure called Universal Proof Graph (UPG) that encodes all possible applications of inference rules over all small propositions abstracted using their bitvector-based truth-table representation. This allows an efficient forward search for solution generation. More interestingly, this allows generating fresh practice problems that have given solution characteristics by performing a backward search in UPG. We obtained around 300 natural deduction problems from various textbooks. Our solution generation procedure can solve many more problems than the traditional forward-chaining based procedure, while our problem generation procedure can efficiently generate several variants with desired characteristics.